<html>
<head><meta charset="utf-8"><title>const types · t-compiler/const-eval · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/index.html">t-compiler/const-eval</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html">const types</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="156617339"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156617339" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156617339">(Jan 22 2019 at 16:21)</a>:</h4>
<p><span class="user-mention" data-user-id="121053">@varkor</span> Just catching up on the const-generics RFC. One thing I am really confused about is your notion of "const types". You seem to take that for granted. I never considered it, and I think it is not necessary. Could you briefly explain what you mean by that? what distinguishes "const" from "non-const" types? (See <a href="https://www.ralfj.de/blog/2018/07/19/const.html" target="_blank" title="https://www.ralfj.de/blog/2018/07/19/const.html">https://www.ralfj.de/blog/2018/07/19/const.html</a> for my previous thoughts on const-ness.)</p>



<a name="156617576"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156617576" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156617576">(Jan 22 2019 at 16:25)</a>:</h4>
<p>I don't think const types are necessary either</p>



<a name="156617588"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156617588" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156617588">(Jan 22 2019 at 16:25)</a>:</h4>
<p>specifically, I see no good reason to make <code>const X: bool = true;</code> and <code>let x = true;</code> have a different type. that's just the same type used in two different contexts.</p>



<a name="156617594"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156617594" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156617594">(Jan 22 2019 at 16:25)</a>:</h4>
<p>at one point, I was considering them, but later I removed them from my model</p>



<a name="156617629"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156617629" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156617629">(Jan 22 2019 at 16:26)</a>:</h4>
<p>so the appendix of <a href="https://varkor.github.io/blog/2019/01/11/const-types-traits-and-implementations-in-Rust.html" target="_blank" title="https://varkor.github.io/blog/2019/01/11/const-types-traits-and-implementations-in-Rust.html">https://varkor.github.io/blog/2019/01/11/const-types-traits-and-implementations-in-Rust.html</a> about the two versions of each type is outdated in that respect?</p>



<a name="156617673"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156617673" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156617673">(Jan 22 2019 at 16:26)</a>:</h4>
<p>wait, I misinterpreted, sorry</p>



<a name="156617715"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156617715" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156617715">(Jan 22 2019 at 16:27)</a>:</h4>
<p>hmm</p>



<a name="156617747"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156617747" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> oli <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156617747">(Jan 22 2019 at 16:27)</a>:</h4>
<p>I think we reached the point of "the set of const types is equal to the set of types" in <a href="https://github.com/rust-rfcs/const-eval/pull/8#issuecomment-452713799" target="_blank" title="https://github.com/rust-rfcs/const-eval/pull/8#issuecomment-452713799">https://github.com/rust-rfcs/const-eval/pull/8#issuecomment-452713799</a></p>



<a name="156617824"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156617824" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156617824">(Jan 22 2019 at 16:28)</a>:</h4>
<p>I think my last view was that there's no need to talk about "const types" in the language itself</p>



<a name="156617844"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156617844" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156617844">(Jan 22 2019 at 16:29)</a>:</h4>
<p>but it makes sense to consider them from the perspective of a type theoretic model</p>



<a name="156617884"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156617884" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156617884">(Jan 22 2019 at 16:29)</a>:</h4>
<p>I disagree, but it may not be necessary for us to agree on the model as long as we agree on the lang design ;)</p>



<a name="156617900"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156617900" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156617900">(Jan 22 2019 at 16:29)</a>:</h4>
<p>but I'm not claiming my model is canonical — I'm sure there are other models that don't view types in that way</p>



<a name="156617972"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156617972" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156617972">(Jan 22 2019 at 16:30)</a>:</h4>
<p>I'm happy as long as there is <em>some</em> model :P</p>



<a name="156618030"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156618030" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156618030">(Jan 22 2019 at 16:31)</a>:</h4>
<p>that said, I would be interested in discussing inaccuracies/simplifications of my model, but if we agree on the design, then it's an unrelated issue, yeah</p>



<a name="156618263"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156618263" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156618263">(Jan 22 2019 at 16:34)</a>:</h4>
<p>(you're right in that I'm writing as if it's "taken for granted" in that post — that was more to attempt to not make the writing more confusing with lots of conditional phrasing, more than an assertion that I think this is the definitive model 😁)</p>



<a name="156624184"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156624184" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156624184">(Jan 22 2019 at 17:53)</a>:</h4>
<p>so basically with the latest RFC and the <code>?const</code> in it, we got 3 levels for generic arguments:</p>
<ul>
<li>must always be const (<code>const Trait</code>)</li>
<li>must be const when called in const context (<code>Trait</code>)</li>
<li>never required to be const (<code>?const Trait</code>)</li>
</ul>
<p>unfortunately this is not in sync with <code>const fn</code> vs <code>fn</code>, the latter is really <code>?const fn</code>... :/</p>
<p>what about trait objects? which kinds of bounds can occur there? is there <code>dyn ?const Trait</code>?</p>



<a name="156624206"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156624206" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156624206">(Jan 22 2019 at 17:53)</a>:</h4>
<p>I'd assume it's like <code>fn</code> ptrs, but then <code>dyn Trait</code> and <code>Trait</code> are very different in const context</p>



<a name="156624269"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156624269" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156624269">(Jan 22 2019 at 17:54)</a>:</h4>
<p>(with the methods of the former not callable)</p>



<a name="156626230"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156626230" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156626230">(Jan 22 2019 at 18:20)</a>:</h4>
<blockquote>
<p>that said, I would be interested in discussing inaccuracies/simplifications of my model, but if we agree on the design, then it's an unrelated issue, yeah</p>
</blockquote>
<p>Here's my biggest issue: the embedding of the const universe in the run-time universe is actually <em>not</em> universal. to use terminology from my blog post, a function being const-safe does <em>not</em> imply it being run-time-safe, because the quantification over the const-invariant of the type occurs both in positive and negative position. So this functor <code>U</code> you describe, I don't think it exists for the function type.</p>
<p>Now I cannot even say if that's an inaccuracy, because your theory is all definitions and no (claimed) theorems -- so, I am not sure what to learn from it TBH. How does it relate to the notion I call "const-safety", which I think is the most important in this entire type system design endavor: Making sure that during const evalaution we don't run code that is unfit for const evaluation.</p>



<a name="156626486"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156626486" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156626486">(Jan 22 2019 at 18:23)</a>:</h4>
<p>To give an example for my claim:</p>
<div class="codehilite"><pre><span></span><span class="k">const</span><span class="w"> </span><span class="k">fn</span> <span class="nf">const_safe_but_not_safe</span><span class="p">(</span><span class="n">x</span>: <span class="kp">&amp;</span><span class="kt">i32</span><span class="p">,</span><span class="w"> </span><span class="n">y</span>: <span class="kt">usize</span><span class="p">)</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="k">unsafe</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">  </span><span class="k">if</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="k">as</span><span class="w"> </span><span class="o">*</span><span class="k">const</span><span class="w"> </span><span class="kt">i32</span><span class="w"> </span><span class="o">==</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="k">as</span><span class="w"> </span><span class="o">*</span><span class="k">const</span><span class="w"> </span><span class="kt">i32</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="c1">// This is unreachable in const context, because `usize` must never be a pointer. Hence we can do whatever we want.</span>
<span class="w">    </span><span class="o">*</span><span class="p">(</span><span class="mi">0</span><span class="k">usize</span><span class="w"> </span><span class="k">as</span><span class="w"> </span><span class="o">*</span><span class="k">mut</span><span class="w"> </span><span class="kt">u8</span><span class="p">)</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="mi">0</span><span class="p">;</span><span class="w"></span>
<span class="w">  </span><span class="p">}</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>
</pre></div>


<p>This function, when called from a safe const context, can never cause an error. From a safe run-time context it can easily cause UB. And yet you claim every <code>const fn</code> can be mapped to a <code>fn</code>.</p>



<a name="156636314"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156636314" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156636314">(Jan 22 2019 at 20:25)</a>:</h4>
<p>is this function callable at run-time though?</p>



<a name="156636452"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156636452" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156636452">(Jan 22 2019 at 20:26)</a>:</h4>
<p>if you can call it, even if it's not safe, then I'm considering it a valid function</p>



<a name="156636475"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156636475" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156636475">(Jan 22 2019 at 20:26)</a>:</h4>
<p>if there are some functions that may <em>only</em> be called at compile-time, then I agree that my model is inaccurate</p>



<a name="156636501"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156636501" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156636501">(Jan 22 2019 at 20:27)</a>:</h4>
<p>if not, though, I'm more concerned about the type system than actual safety</p>



<a name="156636522"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156636522" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156636522">(Jan 22 2019 at 20:27)</a>:</h4>
<p>(which is less important in practice, but still a valuable aspect to consider)</p>



<a name="156636598"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156636598" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156636598">(Jan 22 2019 at 20:28)</a>:</h4>
<blockquote>
<p>because your theory is all definitions and no (claimed) theorems</p>
</blockquote>
<p>mhm, unfortunately I have less time to spend playing around with this than I would like</p>



<a name="156638835"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156638835" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156638835">(Jan 22 2019 at 20:57)</a>:</h4>
<blockquote>
<p>if you can call it, even if it's not safe, then I'm considering it a valid function</p>
</blockquote>
<p>in that case your model does not properly reflect whether functions are safe to call, which is the prime purpose of a type system -- and it is a type (and effect) system we are designing here.</p>



<a name="156638843"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156638843" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156638843">(Jan 22 2019 at 20:57)</a>:</h4>
<blockquote>
<p>if not, though, I'm more concerned about the type system than actual safety</p>
</blockquote>
<p>I agree modelling a type system is valuable, but usually that comes with a claim of type safety. I am not asking for a proof of it, but in your definitions I do not see what the claim would even look like.</p>



<a name="156643414"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156643414" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156643414">(Jan 22 2019 at 21:55)</a>:</h4>
<p>(deleted)</p>



<a name="156643681"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156643681" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156643681">(Jan 22 2019 at 21:58)</a>:</h4>
<p>regardless, how are you proposing the <code>const_safe_but_not_safe</code> function be uncallable at run-time?</p>



<a name="156643698"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156643698" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156643698">(Jan 22 2019 at 21:58)</a>:</h4>
<p>at the moment, it's not represented in the type at all (without some ad hoc rule about <code>usize</code>, etc.)</p>



<a name="156643704"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156643704" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156643704">(Jan 22 2019 at 21:58)</a>:</h4>
<p>so surely the current type system is failing in that regard</p>



<a name="156643846"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156643846" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156643846">(Jan 22 2019 at 22:00)</a>:</h4>
<blockquote>
<p>I agree modelling a type system is valuable, but usually that comes with a claim of type safety.</p>
</blockquote>
<p>Rust's type system is unsound as it stands, so I don't see that a reasonable claim at type safety can be made</p>



<a name="156643865"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156643865" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156643865">(Jan 22 2019 at 22:00)</a>:</h4>
<p>proposing variations on the type system is a different matter</p>



<a name="156643933"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156643933" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156643933">(Jan 22 2019 at 22:01)</a>:</h4>
<p>I wasn't intending to come up with a model suitable for formal verification, etc.</p>



<a name="156643937"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156643937" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156643937">(Jan 22 2019 at 22:01)</a>:</h4>
<p>it's more idealised</p>



<a name="156644017"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156644017" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156644017">(Jan 22 2019 at 22:02)</a>:</h4>
<p>maybe it's true that it's a valid model without <code>unsafe</code>?</p>



<a name="156644222"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156644222" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156644222">(Jan 22 2019 at 22:05)</a>:</h4>
<blockquote>
<p>Rust's type system is unsound as it stands, so I don't see that a reasonable claim at type safety can be made</p>
</blockquote>
<p><span class="user-mention" data-user-id="121053">@varkor</span>  uhm... elaborate?</p>



<a name="156644439"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156644439" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156644439">(Jan 22 2019 at 22:08)</a>:</h4>
<p>you can trivially cause UB</p>



<a name="156644446"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156644446" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156644446">(Jan 22 2019 at 22:08)</a>:</h4>
<p>if you set out to do it</p>



<a name="156644464"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156644464" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156644464">(Jan 22 2019 at 22:08)</a>:</h4>
<p>if you want to prove soundness, it has to be for a subset of the language</p>



<a name="156644716"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156644716" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156644716">(Jan 22 2019 at 22:12)</a>:</h4>
<p>While it's technically correct that Rust's type system does not ensure the type safety of programs involving <code>unsafe</code>, it is also pretty clear that everyone here is deeply aware of it, so I don't see a reason to point it out like that.</p>



<a name="156645173"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156645173" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156645173">(Jan 22 2019 at 22:19)</a>:</h4>
<p>my point is that you can only get so far modelling type safety in the presence of <code>unsafe</code>, so it's not entirely unreasonable to have a model of the type system that ignores it</p>



<a name="156645190"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156645190" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156645190">(Jan 22 2019 at 22:19)</a>:</h4>
<p>more accurate models are more useful, but less accurate ones aren't necessarily not useful</p>



<a name="156645495"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156645495" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156645495">(Jan 22 2019 at 22:23)</a>:</h4>
<p>What you <em>can</em> do with type safety, and with CTFE as well, is to lay out a complete but not-statically-checkable definition of what the desired safety property is (no runtime UB / no code that CTFE can't handle) and then see how well proposed static analyses approximate that end goal, and in particular whether they are sound.</p>



<a name="156645807"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156645807" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156645807">(Jan 22 2019 at 22:27)</a>:</h4>
<p>sure, I don't dispute that</p>



<a name="156645901"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156645901" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156645901">(Jan 22 2019 at 22:28)</a>:</h4>
<p>models that demonstrate soundness for subsets of the language can be useful too, though</p>



<a name="156646014"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156646014" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156646014">(Jan 22 2019 at 22:30)</a>:</h4>
<p>so while a complete model would detail exactly when any behaviour is safe/unsafe/etc., that doesn't obviate other models</p>



<a name="156646101"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156646101" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156646101">(Jan 22 2019 at 22:31)</a>:</h4>
<p>A model for a subset of the language should, however, come with a way to tell when that model applies.</p>



<a name="156646115"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156646115" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156646115">(Jan 22 2019 at 22:31)</a>:</h4>
<p>agreed</p>



<a name="156646144"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156646144" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156646144">(Jan 22 2019 at 22:31)</a>:</h4>
<p>in the model in question, my conjecture is that it could apply for a subset of the language where <code>unsafe</code> doesn't exist</p>



<a name="156646253"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156646253" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156646253">(Jan 22 2019 at 22:33)</a>:</h4>
<p>(which is the context in which Ralf pointed out my draft model was oversimplified)</p>



<a name="156646258"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156646258" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156646258">(Jan 22 2019 at 22:33)</a>:</h4>
<p>I know basically nothing about your model but in general I have a lot of reservation about models that completely ignore unsafe, because unsafe can add new capabilities to safe interfaces, so compositional reasoning is ham-strung</p>



<a name="156646348"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156646348" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156646348">(Jan 22 2019 at 22:34)</a>:</h4>
<p>it's more like a first-pass litmus test</p>



<a name="156646364"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156646364" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156646364">(Jan 22 2019 at 22:34)</a>:</h4>
<p>if a feature doesn't even fit into a model <em>without</em> <code>unsafe</code>, there's no way it's feasible with <code>unsafe</code> as well</p>



<a name="156646389"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156646389" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156646389">(Jan 22 2019 at 22:34)</a>:</h4>
<p>but a feature should definitely be considered in light of <code>unsafe</code> if it seems all right without it</p>



<a name="156646395"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156646395" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156646395">(Jan 22 2019 at 22:35)</a>:</h4>
<p>for a very particular interpretation of "doesn't fit without <code>unsafe</code>"</p>



<a name="156646426"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156646426" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156646426">(Jan 22 2019 at 22:35)</a>:</h4>
<p>well, in any such model</p>



<a name="156646445"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156646445" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156646445">(Jan 22 2019 at 22:35)</a>:</h4>
<p>as long as there exists <em>some</em> (reasonable) model, then it's fine</p>



<a name="156646448"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156646448" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156646448">(Jan 22 2019 at 22:35)</a>:</h4>
<p>for example, a bunch of std APIs seem overly complicated or unnecessary or vacuous if one ignores unsafe</p>



<a name="156646552"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156646552" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156646552">(Jan 22 2019 at 22:36)</a>:</h4>
<p>in <em>any</em> simplification of the language, some features/functions are going to seem unnecessary</p>



<a name="156646561"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156646561" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156646561">(Jan 22 2019 at 22:36)</a>:</h4>
<p>I do think you want as precise a model as possible</p>



<a name="156646579"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156646579" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156646579">(Jan 22 2019 at 22:37)</a>:</h4>
<p>which goes hand-in-hand with the sort of formal verification Ralf, etc. are doing</p>



<a name="156646604"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156646604" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156646604">(Jan 22 2019 at 22:37)</a>:</h4>
<p>I'm really just having fun by trying to define a simplified model from a more type theoretic perspective</p>



<a name="156646605"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156646605" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156646605">(Jan 22 2019 at 22:37)</a>:</h4>
<p>I don't really want anything specific in this discussion, I'm way too behind on all the const trait bounds discussion.</p>



<a name="156646682"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156646682" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156646682">(Jan 22 2019 at 22:38)</a>:</h4>
<p>But ultimately I am curious whether this "const types" idea is giving any useful intuition for the real problem of handling the whole language, and the discussion so far doesn't give that impression</p>



<a name="156646690"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156646690" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156646690">(Jan 22 2019 at 22:38)</a>:</h4>
<p>I think the essence of the discussion at this point is that, though we may have come to it by different reasoning, most people seem reasonably happy with the design of the const trait bounds RFC at the moment</p>



<a name="156646695"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156646695" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156646695">(Jan 22 2019 at 22:38)</a>:</h4>
<p>hmm</p>



<a name="156646709"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156646709" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156646709">(Jan 22 2019 at 22:39)</a>:</h4>
<p>Partly because it doesn't seem there is a precise connection to the more detailed/complete approaches like CTFE safety</p>



<a name="156646741"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156646741" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156646741">(Jan 22 2019 at 22:39)</a>:</h4>
<p>or at least it's not clear to me (nor to Ralf IIUC) what it is</p>



<a name="156646781"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156646781" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156646781">(Jan 22 2019 at 22:39)</a>:</h4>
<p>I kind of expect them to coïncide if it was pushed</p>



<a name="156646834"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156646834" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156646834">(Jan 22 2019 at 22:40)</a>:</h4>
<p>but part of the problem is that it's not well-defined</p>



<a name="156646841"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156646841" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156646841">(Jan 22 2019 at 22:40)</a>:</h4>
<p>(that is, my formulation)</p>



<a name="156646850"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156646850" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156646850">(Jan 22 2019 at 22:40)</a>:</h4>
<p>so it's not easy to make concrete statements about</p>



<a name="156646873"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156646873" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156646873">(Jan 22 2019 at 22:40)</a>:</h4>
<p>it was something to lend myself intuition, and I thought some people might find it more helpful</p>



<a name="156646888"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156646888" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156646888">(Jan 22 2019 at 22:40)</a>:</h4>
<p>I think it very much depends on how you're thinking about it</p>



<a name="156646933"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156646933" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156646933">(Jan 22 2019 at 22:41)</a>:</h4>
<p>if you're concerned with the precise details around CTFE and unsafe, etc., then you want a very accurate model, and having something vaguer and more loosely connected isn't helpful at all</p>



<a name="156646990"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156646990" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156646990">(Jan 22 2019 at 22:42)</a>:</h4>
<p>but if you want to know what "const" means in terms of a programming language in general, I find it helpful to take a wider perspective, and brush over the details</p>



<a name="156647050"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156647050" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156647050">(Jan 22 2019 at 22:43)</a>:</h4>
<p>I think you can get some way just by pretending a language is more "nicely behaved" (for some such definition) than it really is, to get an overall intuition</p>



<a name="156647132"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156647132" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156647132">(Jan 22 2019 at 22:44)</a>:</h4>
<p>I agree that it's about how you're thinking about it, but not like that. The reason I have difficulties with what you're describing (in this channel) is that type systems mostly are an unfortunate approximation, an incomplete proof calculus, for what I <em>actually</em> care about (how programs behave when run) -- at least when talking about languages like Rust, where Curry-Howard is no good. One can then fruitfully restrict attention to subsets of programs or aspects of behavior (e.g., disregard divergence), but it's still very "bottom up".</p>



<a name="156648534"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156648534" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156648534">(Jan 22 2019 at 23:06)</a>:</h4>
<p>yeah, I find the actual run-time behaviour less interesting than the type system in and of itself</p>



<a name="156648553"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156648553" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156648553">(Jan 22 2019 at 23:07)</a>:</h4>
<p>which I completely accept is less useful</p>



<a name="156648567"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156648567" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156648567">(Jan 22 2019 at 23:07)</a>:</h4>
<p>but explains why I'm tending to think about it very differently</p>



<a name="156648580"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156648580" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156648580">(Jan 22 2019 at 23:07)</a>:</h4>
<p>I suppose I'm interested in where the two intersect</p>



<a name="156648665"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156648665" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156648665">(Jan 22 2019 at 23:09)</a>:</h4>
<p>but I can content myself with pretending it's closer to the pure mathematical perspective than it actually is in reality</p>



<a name="156648988"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156648988" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156648988">(Jan 22 2019 at 23:15)</a>:</h4>
<p><span class="user-mention" data-user-id="121053">@varkor</span>  I thought it was generally accepted that <code>unsafe { .. }</code> is a "believe me" construct that you use to do manual "proofs" of type safety and that it is the users responsibility to restore type system invariants, progress &amp; preservation at the boundaries...</p>
<p>Agda and Coq have "believe me" constructs as well; but usually this does not lead anyone to state that Agda is unsound...</p>



<a name="156649057"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156649057" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156649057">(Jan 22 2019 at 23:16)</a>:</h4>
<p>in that case, the fact that the CT model fails for Ralf's example is not important, no?</p>



<a name="156649074"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156649074" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156649074">(Jan 22 2019 at 23:16)</a>:</h4>
<p>I didn't read all of the backlog so idk</p>



<a name="156649081"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156649081" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156649081">(Jan 22 2019 at 23:17)</a>:</h4>
<p>I know of few programming languages that don't have "believe me" constructs of some form</p>



<a name="156649165"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156649165" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156649165">(Jan 22 2019 at 23:19)</a>:</h4>
<p><span class="user-mention" data-user-id="121053">@varkor</span> if we develop a denotational semantics of Rust, what would be the category? For Haskell this is a complete partial order iirc</p>



<a name="156649234"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156649234" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156649234">(Jan 22 2019 at 23:20)</a>:</h4>
<p>some sort of category of partial maps, I'm sure</p>



<a name="156649242"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156649242" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156649242">(Jan 22 2019 at 23:20)</a>:</h4>
<p>though honestly, my interests are far more focused on the type system than the run-time behaviour</p>



<a name="156649312"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156649312" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156649312">(Jan 22 2019 at 23:22)</a>:</h4>
<p><span class="user-mention" data-user-id="121053">@varkor</span>  that seems like a very proof irrelevant perspective =P</p>



<a name="156649412"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156649412" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156649412">(Jan 22 2019 at 23:24)</a>:</h4>
<p>it's distinguishing the type system from the programming language</p>



<a name="156649419"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156649419" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156649419">(Jan 22 2019 at 23:24)</a>:</h4>
<p>you can have a type theory without a run-time semantics (operational or denotational)</p>



<a name="156649754"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156649754" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156649754">(Jan 22 2019 at 23:31)</a>:</h4>
<p><span class="user-mention" data-user-id="121053">@varkor</span>  sure; but if your type theory is not in sync with the dynamic semantics, bad things happen...</p>
<p>Moreover, in a less boring type system (e.g. dependently typed) dynamic semantics become part of the types (well... not really, but at that point you might as well use the normalization rules as the runtime semantics anyways</p>



<a name="156649853"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156649853" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156649853">(Jan 22 2019 at 23:32)</a>:</h4>
<p>LMK if you want to collaborate on a denotational semantics ;)</p>



<a name="156651613"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156651613" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156651613">(Jan 23 2019 at 00:03)</a>:</h4>
<p>ehehe :P some day, some day ;)</p>



<a name="156677397"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156677397" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156677397">(Jan 23 2019 at 10:11)</a>:</h4>
<blockquote>
<p><span class="user-mention silent" data-user-id="121053">@varkor</span> if we develop a denotational semantics of Rust, what would be the category? For Haskell this is a complete partial order iirc</p>
</blockquote>
<p>AFAIK nobody has demonstrated categorical semantics for higher-order imperative (let alone concurrent) languages. one of many reasons why I have big reservations about categorical semantics.</p>



<a name="156677510"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/const%20types/near/156677510" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/const.20types.html#156677510">(Jan 23 2019 at 10:13)</a>:</h4>
<p>also in terms of type systems, AFAIK a categorical treatment of dependent types is a mess at best. I like category theory for some things but I feel that in some PL circles it is awfully overrated.<br>
Anyway, I'll stop ranting now^^</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>